00100	EPISTEMOLOGY, PROOF-CHECKING AND MATHEMATICAL THEORY OF COMPUTATION
00200	
00300	
00400		These three topics are being treated together in this proposal,
00500	because they are being simultaneously advanced in a somewhat unified
00600	effort.  This effort is based on a proof-checker for first order logic
00700	called FOL that is being improved and extended by Richard Weyhrauch,
00800	Bill Glassmire, Arthur Thomas and David Poole.
00900	
01000		Before describing the present state of this work and what is
01100	planned in the next two years, it seems desirable to explain the
01200	rationale of this effort, which is perhaps the Laboratory's major
01300	effort in the theoretical side of artificial intelligence.
01400	
01500	
01600	THE EPISTEMOLOGICAL PART OF ARTIFICIAL INTELLIGENCE
01700	
01800		Artificial intelligence has proved to be, as some people
01900	expected and others didn't, a very difficult scientific subject.
02000	In its first ten years, the limits of what could be done by
02100	straightforward programming on specific intellectual problems
02200	such as games and theorem proving were explored.  Besides that,
02300	a number of ideas for general intelligent systems were also
02400	explored with limited results.
02500	It became clear that computer systems of human intelligence level
02600	were not going to be obtained in one grand rush.  Once this is
02700	understood, it becomes important to try to analyze the artificial
02800	intelligence problem into a collection of subproblems and try
02900	to split off subproblems that can be tackled separately and
03000	whose solution will contribute to the solution of the problem
03100	as a whole.  One such analysis (McCarthy and Hayes 1970) divides
03200	the artificial intelligence problem into a heuristic part and
03300	an epistemological part.
03400	
03500		The heuristic part of the problem was tackled first and
03600	is best understood.